The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

nthtail(n, l) → cond(ge(n, length(l)), n, l)
cond(true, n, l) → l
cond(false, n, l) → tail(nthtail(s(n), l))
tail(nil) → nil
tail(cons(x, l)) → l
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

nthtail(n, l) → cond(ge(n, length(l)), n, l) [1]
cond(true, n, l) → l [1]
cond(false, n, l) → tail(nthtail(s(n), l)) [1]
tail(nil) → nil [1]
tail(cons(x, l)) → l [1]
length(nil) → 0 [1]
length(cons(x, l)) → s(length(l)) [1]
ge(u, 0) → true [1]
ge(0, s(v)) → false [1]
ge(s(u), s(v)) → ge(u, v) [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

nthtail(n, l) → cond(ge(n, length(l)), n, l) [1]
cond(true, n, l) → l [1]
cond(false, n, l) → tail(nthtail(s(n), l)) [1]
tail(nil) → nil [1]
tail(cons(x, l)) → l [1]
length(nil) → 0 [1]
length(cons(x, l)) → s(length(l)) [1]
ge(u, 0) → true [1]
ge(0, s(v)) → false [1]
ge(s(u), s(v)) → ge(u, v) [1]

The TRS has the following type information:

nthtail :: s:0 → nil:cons → nil:cons cond :: true:false → s:0 → nil:cons → nil:cons ge :: s:0 → s:0 → true:false length :: nil:cons → s:0 true :: true:false false :: true:false tail :: nil:cons → nil:cons s :: s:0 → s:0 nil :: nil:cons cons :: a → nil:cons → nil:cons 0 :: s:0

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:
none

And the following fresh constants:

const

(6) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: nthtail(n, l) → cond(ge(n, length(l)), n, l) [1] cond(true, n, l) → l [1] cond(false, n, l) → tail(nthtail(s(n), l)) [1] tail(nil) → nil [1] tail(cons(x, l)) → l [1] length(nil) → 0 [1] length(cons(x, l)) → s(length(l)) [1] ge(u, 0) → true [1] ge(0, s(v)) → false [1] ge(s(u), s(v)) → ge(u, v) [1] The TRS has the following type information: nthtail :: s:0 → nil:cons → nil:cons cond :: true:false → s:0 → nil:cons → nil:cons ge :: s:0 → s:0 → true:false length :: nil:cons → s:0 true :: true:false false :: true:false tail :: nil:cons → nil:cons s :: s:0 → s:0 nil :: nil:cons cons :: a → nil:cons → nil:cons 0 :: s:0 const :: a Rewrite Strategy: INNERMOST

(7) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

true => 1
false => 0
nil => 0
0 => 0
const => 0

(8) Obligation:

Complexity RNTS consisting of the following rules:

cond(z, z', z'') -{ 1 }→ l :|: n >= 0, z = 1, z' = n, l >= 0, z'' = l
cond(z, z', z'') -{ 1 }→ tail(nthtail(1 + n, l)) :|: n >= 0, z' = n, l >= 0, z = 0, z'' = l
ge(z, z') -{ 1 }→ ge(u, v) :|: v >= 0, z' = 1 + v, z = 1 + u, u >= 0
ge(z, z') -{ 1 }→ 1 :|: z = u, z' = 0, u >= 0
ge(z, z') -{ 1 }→ 0 :|: v >= 0, z' = 1 + v, z = 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 1 }→ 1 + length(l) :|: x >= 0, l >= 0, z = 1 + x + l
nthtail(z, z') -{ 1 }→ cond(ge(n, length(l)), n, l) :|: z' = l, n >= 0, z = n, l >= 0
tail(z) -{ 1 }→ l :|: x >= 0, l >= 0, z = 1 + x + l
tail(z) -{ 1 }→ 0 :|: z = 0

Only complete derivations are relevant for the runtime complexity.

(9) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V1, V4),0,[nthtail(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V4),0,[cond(V, V1, V4, Out)],[V >= 0,V1 >= 0,V4 >= 0]). eq(start(V, V1, V4),0,[tail(V, Out)],[V >= 0]). eq(start(V, V1, V4),0,[length(V, Out)],[V >= 0]). eq(start(V, V1, V4),0,[ge(V, V1, Out)],[V >= 0,V1 >= 0]). eq(nthtail(V, V1, Out),1,[length(V3, Ret01),ge(V2, Ret01, Ret0),cond(Ret0, V2, V3, Ret)],[Out = Ret,V1 = V3,V2 >= 0,V = V2,V3 >= 0]). eq(cond(V, V1, V4, Out),1,[],[Out = V5,V6 >= 0,V = 1,V1 = V6,V5 >= 0,V4 = V5]). eq(cond(V, V1, V4, Out),1,[nthtail(1 + V7, V8, Ret02),tail(Ret02, Ret1)],[Out = Ret1,V7 >= 0,V1 = V7,V8 >= 0,V = 0,V4 = V8]). eq(tail(V, Out),1,[],[Out = 0,V = 0]). eq(tail(V, Out),1,[],[Out = V9,V10 >= 0,V9 >= 0,V = 1 + V10 + V9]). eq(length(V, Out),1,[],[Out = 0,V = 0]). eq(length(V, Out),1,[length(V11, Ret11)],[Out = 1 + Ret11,V12 >= 0,V11 >= 0,V = 1 + V11 + V12]). eq(ge(V, V1, Out),1,[],[Out = 1,V = V13,V1 = 0,V13 >= 0]). eq(ge(V, V1, Out),1,[],[Out = 0,V14 >= 0,V1 = 1 + V14,V = 0]). eq(ge(V, V1, Out),1,[ge(V15, V16, Ret2)],[Out = Ret2,V16 >= 0,V1 = 1 + V16,V = 1 + V15,V15 >= 0]). input_output_vars(nthtail(V,V1,Out),[V,V1],[Out]). input_output_vars(cond(V,V1,V4,Out),[V,V1,V4],[Out]). input_output_vars(tail(V,Out),[V],[Out]). input_output_vars(length(V,Out),[V],[Out]). input_output_vars(ge(V,V1,Out),[V,V1],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. recursive : [ge/3]
1. recursive : [length/2]
2. non_recursive : [tail/2]
3. recursive [non_tail] : [cond/4,nthtail/3]
4. non_recursive : [start/3]

#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into ge/3
1. SCC is partially evaluated into length/2
2. SCC is partially evaluated into tail/2
3. SCC is partially evaluated into nthtail/3
4. SCC is partially evaluated into start/3

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations ge/3
* CE 16 is refined into CE [17]
* CE 14 is refined into CE [18]
* CE 15 is refined into CE [19]


### Cost equations --> "Loop" of ge/3
* CEs [18] --> Loop 12
* CEs [19] --> Loop 13
* CEs [17] --> Loop 14

### Ranking functions of CR ge(V,V1,Out)
* RF of phase [14]: [V,V1]

#### Partial ranking functions of CR ge(V,V1,Out)
* Partial RF of phase [14]:
- RF of loop [14:1]:
V
V1


### Specialization of cost equations length/2
* CE 13 is refined into CE [20]
* CE 12 is refined into CE [21]


### Cost equations --> "Loop" of length/2
* CEs [21] --> Loop 15
* CEs [20] --> Loop 16

### Ranking functions of CR length(V,Out)
* RF of phase [16]: [V]

#### Partial ranking functions of CR length(V,Out)
* Partial RF of phase [16]:
- RF of loop [16:1]:
V


### Specialization of cost equations tail/2
* CE 11 is refined into CE [22]
* CE 10 is refined into CE [23]


### Cost equations --> "Loop" of tail/2
* CEs [22] --> Loop 17
* CEs [23] --> Loop 18

### Ranking functions of CR tail(V,Out)

#### Partial ranking functions of CR tail(V,Out)


### Specialization of cost equations nthtail/3
* CE 9 is refined into CE [24,25]
* CE 8 is refined into CE [26,27,28,29]


### Cost equations --> "Loop" of nthtail/3
* CEs [29] --> Loop 19
* CEs [28] --> Loop 20
* CEs [27] --> Loop 21
* CEs [26] --> Loop 22
* CEs [25] --> Loop 23
* CEs [24] --> Loop 24

### Ranking functions of CR nthtail(V,V1,Out)
* RF of phase [19]: [-V+V1]
* RF of phase [20]: [-V+V1]

#### Partial ranking functions of CR nthtail(V,V1,Out)
* Partial RF of phase [19]:
- RF of loop [19:1]:
-V+V1
* Partial RF of phase [20]:
- RF of loop [20:1]:
-V+V1


### Specialization of cost equations start/3
* CE 3 is refined into CE [30]
* CE 2 is refined into CE [31,32,33,34]
* CE 4 is refined into CE [35,36,37,38]
* CE 5 is refined into CE [39,40]
* CE 6 is refined into CE [41,42]
* CE 7 is refined into CE [43,44,45,46]


### Cost equations --> "Loop" of start/3
* CEs [36,44] --> Loop 25
* CEs [30,37,38,40,42,45,46] --> Loop 26
* CEs [31,32,33,34,35,39,41,43] --> Loop 27

### Ranking functions of CR start(V,V1,V4)

#### Partial ranking functions of CR start(V,V1,V4)


Computing Bounds
=====================================

#### Cost of chains of ge(V,V1,Out):
* Chain [[14],13]: 1*it(14)+1
Such that:it(14) =< V

with precondition: [Out=0,V>=1,V1>=V+1]

* Chain [[14],12]: 1*it(14)+1
Such that:it(14) =< V1

with precondition: [Out=1,V1>=1,V>=V1]

* Chain [13]: 1
with precondition: [V=0,Out=0,V1>=1]

* Chain [12]: 1
with precondition: [V1=0,Out=1,V>=0]


#### Cost of chains of length(V,Out):
* Chain [[16],15]: 1*it(16)+1
Such that:it(16) =< V

with precondition: [Out>=1,V>=Out]

* Chain [15]: 1
with precondition: [V=0,Out=0]


#### Cost of chains of tail(V,Out):
* Chain [18]: 1
with precondition: [V=0,Out=0]

* Chain [17]: 1
with precondition: [Out>=0,V>=Out+1]


#### Cost of chains of nthtail(V,V1,Out):
* Chain [[20],[19],23]: 10*it(19)+2*s(1)+4*s(7)+4
Such that:aux(9) =< -V+V1
aux(10) =< V1
it(19) =< aux(9)
s(1) =< aux(10)
s(7) =< it(19)*aux(10)

with precondition: [Out=0,V>=1,V1>=V+2]

* Chain [[19],23]: 5*it(19)+2*s(1)+2*s(7)+4
Such that:it(19) =< -V+V1
aux(5) =< V1
s(1) =< aux(5)
s(7) =< it(19)*aux(5)

with precondition: [V>=1,Out>=0,V1>=V+1,V1>=Out+1]

* Chain [24]: 4
with precondition: [V1=0,Out=0,V>=0]

* Chain [23]: 2*s(1)+4
Such that:aux(1) =< V1
s(1) =< aux(1)

with precondition: [V1=Out,V>=1,V1>=1]

* Chain [22,[20],[19],23]: 13*it(19)+4*s(7)+9
Such that:aux(11) =< V1
it(19) =< aux(11)
s(7) =< it(19)*aux(11)

with precondition: [V=0,Out=0,V1>=3]

* Chain [22,[19],23]: 8*it(19)+2*s(7)+9
Such that:aux(12) =< V1
it(19) =< aux(12)
s(7) =< it(19)*aux(12)

with precondition: [V=0,Out=0,V1>=2]

* Chain [21,[19],23]: 8*it(19)+2*s(7)+9
Such that:aux(13) =< V1
it(19) =< aux(13)
s(7) =< it(19)*aux(13)

with precondition: [V=0,Out>=0,V1>=Out+2]

* Chain [21,23]: 3*s(1)+9
Such that:aux(14) =< V1
s(1) =< aux(14)

with precondition: [V=0,Out>=0,V1>=Out+1]


#### Cost of chains of start(V,V1,V4):
* Chain [27]: 30*s(39)+10*s(40)+12*s(41)+32*s(50)+8*s(51)+9
Such that:s(49) =< V1
aux(18) =< -V1+V4
aux(19) =< V4
s(39) =< aux(18)
s(40) =< aux(19)
s(41) =< s(39)*aux(19)
s(50) =< s(49)
s(51) =< s(50)*s(49)

with precondition: [V=0]

* Chain [26]: 15*s(54)+7*s(55)+6*s(56)+2*s(59)+4
Such that:s(52) =< -V+V1
aux(20) =< V
aux(21) =< V1
s(59) =< aux(20)
s(55) =< aux(21)
s(54) =< s(52)
s(56) =< s(54)*aux(21)

with precondition: [V>=1]

* Chain [25]: 4
with precondition: [V1=0,V>=0]


Closed-form bounds of start(V,V1,V4):
-------------------------------------
* Chain [27] with precondition: [V=0]
- Upper bound: nat(V1)*32+9+nat(V1)*8*nat(V1)+nat(V4)*10+nat(V4)*12*nat(-V1+V4)+nat(-V1+V4)*30
- Complexity: n^2
* Chain [26] with precondition: [V>=1]
- Upper bound: 2*V+4+nat(V1)*7+nat(V1)*6*nat(-V+V1)+nat(-V+V1)*15
- Complexity: n^2
* Chain [25] with precondition: [V1=0,V>=0]
- Upper bound: 4
- Complexity: constant

### Maximum cost of start(V,V1,V4): nat(V1)*7+max([nat(V1)*6*nat(-V+V1)+2*V+nat(-V+V1)*15,nat(V1)*25+5+nat(V1)*8*nat(V1)+nat(V4)*10+nat(V4)*12*nat(-V1+V4)+nat(-V1+V4)*30])+4
Asymptotic class: n^2
* Total analysis performed in 338 ms.

(10) BOUNDS(1, n^2)